w_sends(e;l)
== sends(product-deq(Id;;IdDeq;NatDeq);IdLnkDeq;e.w-pred(w;e);e.w-info(w;e);e.
== val(e);(TERMOF{w-order-axioms:ObjectId, 1:l, i:l}(w,p)).1;e;l) 

latex

---

clarification:

w_sends{i:l}
w_sends(w; p; e; l)
== sends(product-deq(Id;;IdDeq;NatDeq);IdLnkDeq;e.w-pred(w;e);e.w-info(w;e);e.w-eval
== (w; e);(TERMOF{w-order-axioms:ObjectId, 1:l, i:l}(w,p)).1;e;l) 

latex

Definitions	sends(dE;dL;pred?;info;val;p;e;l), product-deq(A;B;a;b), Id, , IdDeq, NatDeq, IdLnkDeq, w-pred(w;e), w-info(w;e), x.A(x), val(e), t.1, f(a), w-order-axioms
FDL editor aliases	w_sends